import java.util.*;
import java.io.*;

class DPLLclass { 
	public static boolean isSatisfiable(ArrayList clauses) {
		// requires clauses to be an Array List of int arrays
		// first element of the int array denotes how long the actual clause is, in terms of literals

		int[] model = new int[65]; // 65 since model[0] is unused since I forgot and was too lazy to change it
		for(int i=0; i<65; i++){
			model[i] = -1;
		}

		int claus[]; // a single clause
		for(int i=0; i<clauses.size(); i++){
			claus = (int[])clauses.get(i);
			if(claus[0] == 1) { // unit clause
				if(model[Math.abs(claus[1])] < 0) {
					if(claus[1] > 0)  model[Math.abs(claus[1])] = 1;
					else model[Math.abs(claus[1])] = 0;
				} else { // already assigned unit literal, is there a contradiction? 
					// ...this is probably not actually necessary here but I wrote it so I'm keepin' it
					if(model[Math.abs(claus[1])] == 0 && claus[1] > 0) return false;
					if(model[Math.abs(claus[1])] == 1 && claus[1] < 0) return false;
				}
			}
		}

		return DPLL(clauses, model);


	}

	public static boolean DPLL(ArrayList clauses, int[] model){
		int foundUnknown;
		boolean foundTrue;
		int claus[];
		for(int i=0; i<clauses.size(); i++){
			//System.out.println("Clause check: " + i);
			claus = (int[])clauses.get(i);
			//System.out.println(claus[i]);

			foundUnknown = -1;
			foundTrue = false;
			for(int j = 1; j <= claus[0]; j++){
				if(model[Math.abs(claus[j])] == 1 && claus[j] > 0 || model[Math.abs(claus[j])] == 0 && claus[j] < 0){
					// a true literal has been found
					//System.out.println("True " + j + " " + model[Math.abs(claus[j])]);
					foundTrue = true;
					j = claus[0] + 1; // or break or whatever
				} else if(model[Math.abs(claus[j])] == -1 && foundUnknown < 0) {
					// first unknown found in the literal is remembered
					foundUnknown = j;
				}
			}
			if(foundUnknown < 0 && !foundTrue) { // no unknowns or trues found, so everything false
				/*for(int j=1; j<20; j++){
					System.out.print(model[j] + " ");
				}*/
				//System.out.println("False found, clause " + i);
				return false; 
			}
			if(!foundTrue) { // unknown found, no trues found
				//System.out.println("Unknown " + foundUnknown + " " + claus[foundUnknown]);

				int[] cop = new int[model.length];
				System.arraycopy( model, 0, cop, 0, model.length );

				cop[Math.abs(claus[foundUnknown])] = 1;
				if(DPLL(clauses, cop)) return true;
				cop[Math.abs(claus[foundUnknown])] = 0;
				return DPLL(clauses, cop);
			} // everything true
		}
		/*for(int j=1; j<20; j++){
			System.out.print(model[j] + " ");
		}*/
		return true;
	}
}

